This disclosure relates generally to verification of circuit designs, and more specifically to equivalence checking of circuit designs.
Over the last 30 years, the complexity of integrated circuits has increased greatly. This increase in complexity has exacerbated the difficulty of verifying circuit designs. In a typical integrated circuit design process, which includes many steps, the verification step may consume approximately 70-80% of the total time and resources. Aspects of the circuit design such as time-to-market and profit margin greatly depend on the verification step. As a result, flaws in the design that are not found during the verification step can have significant economic impact by increasing time-to-market and reducing profit margins.
As the complexity in circuit design has increased, there has been a corresponding improvement in various kinds of verification and debugging techniques. In fact, these verification and debugging techniques have evolved from relatively simple transistor circuit-level simulation (in the early 1970s) to logic gate-level simulation (in the late 1980s) to the current art that uses Register Transfer Language (RTL)-level simulation. RTL describes the registers of a computer or digital electronic system and the way in which data are transferred among them.
Existing verification and debugging tools are used in the design flow of a circuit. The design flow begins with the creation of a circuit design at the RTL level using RTL source code. The RTL source code is specified according to a Hardware Description Language (HDL), such as Verilog HDL or VHDL. Circuit designers use high-level hardware description languages because of the size and complexity of modern integrated circuits. Circuit designs are developed in a high-level language using computer-implemented software applications, which enable a user to use text-editing and graphical design tools to create a HDL-based design.
In the design flow, creation of the RTL source code is followed by verification of the design to check if the RTL source code meets various design specifications. Formal verification is one such technique for verifying the circuit design. Formal verification uses mathematical techniques to prove that, under a set of constraints, a design property is either always correct or to provide an example condition (called a counterexample) that demonstrates the property is false. Tools that use formal methods to verify RTL source code and design properties are known as “model checkers.” Design properties to be verified include specifications and/or requirements that must be satisfied by the circuit design. Since mathematical properties define the design requirements in pure mathematical terms, this enables analysis of all possible valid inputs for a given circuit and is akin to an exhaustive simulation.
One type of verification that is often performed on circuit designs is equivalence checking. Equivalence checking is performed to determine whether two designs exhibit the same functional behavior. This type of verification is often used, for example, when a circuit is modified during the design process, and there is a need to make sure that the modified (implementation or “IMP”) version of the circuit is functionality equivalent to a baseline (specification or “SPEC”) version of the circuit. One reason to perform this type of check is to make sure that the IMP version of a circuit (e.g., that has been modified and/or includes new features) will function properly and be backwards compatible in the context of an existing circuit design.
“Sequential” equivalence checking (SEC) is performed to verify whether two designs exhibit the same behavior at design interfaces. This type of equivalence check ignores internal functional behaviors at state elements, and only checks whether outputs match between the two designs. This is in contrast to combinational equivalence checking (CEC) that check whether two designs exhibit the same functional behavior at all state elements.
The problem with traditional sequential equivalency checking approaches is that they cannot function properly when the two designs are not matchable on a cycle-by-cycle basis. This occurs, for example, in the context of designs whose interface validity is governed by handshake protocols. In this circumstance, the traditional equivalency checking approaches will fail to determine whether the two designs are equivalent at their design interfaces, since there will likely be discrepancies on a cycle basis, regardless of whether the functionality matches between the two designs. Similarly, verification of worst-case performance delays between such designs was not possible before with traditional sequential equivalency checking solutions.
Therefore, there is a need for an improved approach to perform equivalency checking of circuit designs that address these and other problems.